Design verification, the process of validating the functionality of a design against its specification, is a crucial step in today's design flows. Still, today's large system-on-chip (SoC) integrated circuits (ICs) are only partially verified prior to tapeout, i.e., signing-off for preparation of masks and manufacturing, due to the complexities of the designs as well as the time and resources needed to conclude such a daunting task. This complexity forced designers to rely on coverage, design knowledge, and other metrics to decide when to conclude the verification effort and to declare an IC “verified”. Formal verification, as opposed to simulation, is an exhaustive verification technique often applied to fully verify specific, local functionality of a well-defined portion of an IC design, for example, a communication protocol. This verification is typically undertaken by verification experts who spend significant efforts to verify a specific aspect of the functionality of a design.
In recent years, major advances in the automatic application of formal verification expanded this technology to register-transfer level (RTL) designers who cannot afford the extensive time, effort and expertise required for verifying their design functionality. Automatic formal verification techniques now apply to various problems including clock-domain crossing (CDC), timing exception, power reduction and verification, and static analysis of RTL design, and can target the verification of thousands of properties in days. While formal verification of complex ICs is exhaustive, it usually requires significant time and memory resources to provide conclusive results. When resources are exhausted, current formal verification flows provide inconclusive results. For some formal engines, some information on the depth of analysis might be provided to the user. This information is usually insufficient for the user to make an educated decision on whether to increase system resources or to assume that the system is “reasonably” verified.
For example, formal CDC verification has produced mixed results. On one hand, it can detect functional failures and report them. On the other hand, it is time consuming, since a major effort is required to understand, debug and close any kind of failure reported. The difficulty stems from the fact that CDC verification requires structural as well as functional verification. Synchronization involves structure as well as functionality and both must be properly verified before a tapeout can take place. Incorrectly waiving a reported failure might result in missing a design bug that will manifest itself when the manufactured IC is tested or deployed within a system.
When current automatic formal verification flows exhaust allocated memory and time resources, they provide inconclusive results. This indicates that the analysis was not able to find a design defect, but at the same time it was not able to cover the full state space. As side information, some flows provide the depth to which the analysis was carried. While this information is useful, it is very hard for designers using automatic formal verification flows to correctly interpret this information and decide whether the property can be waived. This is due to the fact that this information is formal analysis-centric.
There is therefore a need in the art for a functional verification solution that can provide the user with design-centric metrics that can be used to catch real design problems. Furthermore, it would be advantageous if such a solution executes in a reasonable amount of time and resource. Such a solution should go beyond the results provided by prior art formal approaches and guide the designer of an IC while analyzing inconclusive properties.